COM: sqequal com

COM: sq type com

ABS: SQType(T)

STM: int sq

STM: nat sq

STM: bool sq

STM: atom sq

COM: case ite com

STM: bool sim true

STM: bool sim false

STM: eq int eq true intro

STM: eq int eq false intro

STM: lt int eq true elim

STM: lt int eq false elim

STM: eq atom eq true elim

STM: eq atom eq false elim

STM: eq int eq true elim sqequal

STM: eq int eq false elim sqequal

STM: lt int eq true elim sqequal

STM: lt int eq false elim sqequal

STM: eq atom eq true elim sqequal

STM: eq atom eq false elim sqequal

STM: bool cases sqequal

COM: sqequal 1 end